Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Mod

public class Mod {
  public static void main(String[] args) {
    int x = args[0].length();
    int y = args[1].length();
    mod(x, y);
  }
  public static int mod(int x, int y) {
   
    while (x >= y && y > 0) {
      x = minus(x,y);
     
    }
    return x;
  }

  public static int minus(int x, int y) {
    while (y != 0) {
      if (y > 0)  {
        y--;
        x--;
      } else  {
        y++;
        x++;
      }
    }
    return x;
  }

}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Mod.main([Ljava/lang/String;)V: Graph of 161 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

---

Log for SCC 0:

Generated 34 rules for P and 8 rules for R.

Combined rules. Obtained 3 rules for P and 0 rules for R.

Filtered ground terms:

944_0_minus_EQ(x1, x2, x3, x4) → 944_0_minus_EQ(x2, x3, x4)

Filtered duplicate args:

944_0_minus_EQ(x1, x2, x3) → 944_0_minus_EQ(x1, x3)
944_1_mod_InvokeMethod(x1, x2, x3) → 944_1_mod_InvokeMethod(x1, x3)

Combined rules. Obtained 3 rules for P and 0 rules for R.

Finished conversion. Obtained 3 rules for P and 0 rules for R. System has predefined symbols.

(4) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(0): 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(x1[0] < 0, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])
(1): COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]), x2[1])
(2): 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(x1[2] > 0, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])
(3): COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]), x2[3])
(4): 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(x3[4] > 0 && x3[4] <= x0[4], 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])
(5): COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])

(0) -> (1), if ((x1[0] < 0 →^* TRUE)∧(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]))∧(x2[0] →^* x2[1]))

(1) -> (0), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]))∧(x2[1] →^* x2[0]))

(1) -> (2), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]))∧(x2[1] →^* x2[2]))

(1) -> (4), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]))∧(x2[1] →^* x3[4]))

(2) -> (3), if ((x1[2] > 0 →^* TRUE)∧(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]))∧(x2[2] →^* x2[3]))

(3) -> (0), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]))∧(x2[3] →^* x2[0]))

(3) -> (2), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]))∧(x2[3] →^* x2[2]))

(3) -> (4), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]))∧(x2[3] →^* x3[4]))

(4) -> (5), if ((x3[4] > 0 && x3[4] <= x0[4] →^* TRUE)∧(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]))∧(x3[4] →^* x3[5]))

(5) -> (0), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]))∧(x3[5] →^* x2[0]))

(5) -> (2), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]))∧(x3[5] →^* x2[2]))

(5) -> (4), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]))∧(x3[5] →^* x3[4]))

The set Q is empty.

(5) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) → COND_944_2_MAIN_INVOKEMETHOD(<(x1, 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) the following chains were created:

• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]), COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1]) which results in the following constraint:
  

  (1)    (<(x1[0], 0)=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1])∧x2[0]=x2[1] ⇒ 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥NonInfC∧944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])∧(U^Increasing(COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])), ≥))

  
  
  We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
  

  (2)    (<(x1[0], 0)=TRUE ⇒ 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥NonInfC∧944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])∧(U^Increasing(COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[(-1)bso_29] ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[(-1)bso_29] ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] + [bni_28]x0[0] ≥ 0∧[(-1)bso_29] ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (6)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])), ≥)∧0 = 0∧[bni_28] = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (x1[0] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])), ≥)∧0 = 0∧[bni_28] = 0∧[(-1)Bound*bni_28] + [bni_28]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

  
  
  

For Pair COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0, 1), +(x1, 1)), x2), x2) the following chains were created:

• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]), COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1]), 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) which results in the following constraint:
  

  (8)    (<(x1[0], 0)=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1])∧x2[0]=x2[1]∧944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0]1, x1[0]1), x2[0]1)∧x2[1]=x2[0]1 ⇒ COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥))

  
  
  We simplified constraint (8) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (9)    (<(x1[0], 0)=TRUE ⇒ COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[0], 1), +(x1[0], 1)), x2[0]), x2[0])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥))

  
  
  We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (10)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (11)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (12)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (13)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (14)    (x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)Bound*bni_30] + [bni_30]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  
  
  
• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]), COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1]), 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) which results in the following constraint:
  

  (15)    (<(x1[0], 0)=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1])∧x2[0]=x2[1]∧944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2])∧x2[1]=x2[2] ⇒ COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥))

  
  
  We simplified constraint (15) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (16)    (<(x1[0], 0)=TRUE ⇒ COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[0], 1), +(x1[0], 1)), x2[0]), x2[0])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥))

  
  
  We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (17)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (18)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (19)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (19) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (20)    ([-1] + [-1]x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (20) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (21)    (x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)Bound*bni_30] + [bni_30]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  
  
  
• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]), COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1]), 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) which results in the following constraint:
  

  (22)    (<(x1[0], 0)=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1])∧x2[0]=x2[1]∧944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4])∧x2[1]=x3[4] ⇒ COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥))

  
  
  We simplified constraint (22) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (23)    (<(x1[0], 0)=TRUE∧+(x1[0], 1)=0 ⇒ COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[0], 1), +(x1[0], 1)), x2[0]), x2[0])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥))

  
  
  We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (24)    ([-1] + [-1]x1[0] ≥ 0∧x1[0] + [1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (25)    ([-1] + [-1]x1[0] ≥ 0∧x1[0] + [1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (26)    ([-1] + [-1]x1[0] ≥ 0∧x1[0] + [1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] + [bni_30]x0[0] ≥ 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (26) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (27)    ([-1] + [-1]x1[0] ≥ 0∧x1[0] + [1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (28)    (x1[0] ≥ 0∧[-1]x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)Bound*bni_30] + [bni_30]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  
  
  We simplified constraint (28) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (29)    (0 ≥ 0∧0 ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)Bound*bni_30] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

  
  
  

For Pair 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1, 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) the following chains were created:

• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]), COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3]) which results in the following constraint:
  

  (30)    (>(x1[2], 0)=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3])∧x2[2]=x2[3] ⇒ 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥NonInfC∧944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])∧(U^Increasing(COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])), ≥))

  
  
  We simplified constraint (30) using rules (I), (II), (IV) which results in the following new constraint:
  

  (31)    (>(x1[2], 0)=TRUE ⇒ 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥NonInfC∧944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])∧(U^Increasing(COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])), ≥))

  
  
  We simplified constraint (31) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (32)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[(-1)bso_33] ≥ 0)

  
  
  We simplified constraint (32) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (33)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[(-1)bso_33] ≥ 0)

  
  
  We simplified constraint (33) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (34)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] + [bni_32]x0[2] ≥ 0∧[(-1)bso_33] ≥ 0)

  
  
  We simplified constraint (34) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (35)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])), ≥)∧0 = 0∧[bni_32] = 0∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

  
  
  We simplified constraint (35) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (36)    (x1[2] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])), ≥)∧0 = 0∧[bni_32] = 0∧[(-2)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

  
  
  

For Pair COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0, -1), +(x1, -1)), x2), x2) the following chains were created:

• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]), COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3]), 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) which results in the following constraint:
  

  (37)    (>(x1[2], 0)=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3])∧x2[2]=x2[3]∧944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0])∧x2[3]=x2[0] ⇒ COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥))

  
  
  We simplified constraint (37) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (38)    (>(x1[2], 0)=TRUE ⇒ COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[2], -1), +(x1[2], -1)), x2[2]), x2[2])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥))

  
  
  We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (39)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (40)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (41)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (41) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (42)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧0 = 0∧[bni_34] = 0∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (42) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (43)    (x1[2] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧0 = 0∧[bni_34] = 0∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  
  
  
• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]), COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3]), 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) which results in the following constraint:
  

  (44)    (>(x1[2], 0)=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3])∧x2[2]=x2[3]∧944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2]1, x1[2]1), x2[2]1)∧x2[3]=x2[2]1 ⇒ COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥))

  
  
  We simplified constraint (44) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (45)    (>(x1[2], 0)=TRUE ⇒ COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[2], -1), +(x1[2], -1)), x2[2]), x2[2])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥))

  
  
  We simplified constraint (45) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (46)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (46) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (47)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (47) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (48)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (48) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (49)    (x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧0 = 0∧[bni_34] = 0∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (49) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (50)    (x1[2] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧0 = 0∧[bni_34] = 0∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  
  
  
• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]), COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3]), 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) which results in the following constraint:
  

  (51)    (>(x1[2], 0)=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3])∧x2[2]=x2[3]∧944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4])∧x2[3]=x3[4] ⇒ COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥))

  
  
  We simplified constraint (51) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (52)    (>(x1[2], 0)=TRUE∧+(x1[2], -1)=0 ⇒ COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[2], -1), +(x1[2], -1)), x2[2]), x2[2])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥))

  
  
  We simplified constraint (52) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (53)    (x1[2] + [-1] ≥ 0∧x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (53) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (54)    (x1[2] + [-1] ≥ 0∧x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (54) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (55)    (x1[2] + [-1] ≥ 0∧x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] + [bni_34]x0[2] ≥ 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (55) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (56)    (x1[2] + [-1] ≥ 0∧x1[2] + [-1] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧0 = 0∧[bni_34] = 0∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  
  
  We simplified constraint (56) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (57)    (x1[2] ≥ 0∧x1[2] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧0 = 0∧[bni_34] = 0∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  
  
  

For Pair 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0, 0), x3), x3) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3, 0), <=(x3, x0)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, 0), x3), x3) the following chains were created:

• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]), COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5]) which results in the following constraint:
  

  (58)    (&&(>(x3[4], 0), <=(x3[4], x0[4]))=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5])∧x3[4]=x3[5] ⇒ 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])≥NonInfC∧944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])≥COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])∧(U^Increasing(COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])), ≥))

  
  
  We simplified constraint (58) using rules (I), (II), (IV), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:
  

  (59)    (>(x3[4], 0)=TRUE∧<=(x3[4], x0[4])=TRUE ⇒ 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])≥NonInfC∧944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])≥COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])∧(U^Increasing(COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])), ≥))

  
  
  We simplified constraint (59) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (60)    (x3[4] + [-1] ≥ 0∧x0[4] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [bni_36]x0[4] ≥ 0∧[(-1)bso_37] ≥ 0)

  
  
  We simplified constraint (60) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (61)    (x3[4] + [-1] ≥ 0∧x0[4] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [bni_36]x0[4] ≥ 0∧[(-1)bso_37] ≥ 0)

  
  
  We simplified constraint (61) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (62)    (x3[4] + [-1] ≥ 0∧x0[4] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [bni_36]x0[4] ≥ 0∧[(-1)bso_37] ≥ 0)

  
  
  We simplified constraint (62) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (63)    (x3[4] ≥ 0∧x0[4] + [-1] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])), ≥)∧[(-1)bni_36 + (-1)Bound*bni_36] + [bni_36]x0[4] ≥ 0∧[(-1)bso_37] ≥ 0)

  
  
  We simplified constraint (63) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (64)    (x3[4] ≥ 0∧x0[4] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])), ≥)∧[(-1)Bound*bni_36] + [bni_36]x3[4] + [bni_36]x0[4] ≥ 0∧[(-1)bso_37] ≥ 0)

  
  
  

For Pair COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, 0), x3), x3) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x3), x3), x3) the following chains were created:

• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]), COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5]), 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) which results in the following constraint:
  

  (65)    (&&(>(x3[4], 0), <=(x3[4], x0[4]))=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5])∧x3[4]=x3[5]∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0])∧x3[5]=x2[0] ⇒ COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥))

  
  
  We simplified constraint (65) using rules (I), (II), (III), (IV), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:
  

  (66)    (>(x3[4], 0)=TRUE∧<=(x3[4], x0[4])=TRUE ⇒ COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], x3[4]), x3[4]), x3[4])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥))

  
  
  We simplified constraint (66) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (67)    (x3[4] + [-1] ≥ 0∧x0[4] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x0[4] ≥ 0∧[(-1)bso_39] + x3[4] ≥ 0)

  
  
  We simplified constraint (67) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (68)    (x3[4] + [-1] ≥ 0∧x0[4] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x0[4] ≥ 0∧[(-1)bso_39] + x3[4] ≥ 0)

  
  
  We simplified constraint (68) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (69)    (x3[4] + [-1] ≥ 0∧x0[4] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x0[4] ≥ 0∧[(-1)bso_39] + x3[4] ≥ 0)

  
  
  We simplified constraint (69) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (70)    (x3[4] ≥ 0∧x0[4] + [-1] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x0[4] ≥ 0∧[1 + (-1)bso_39] + x3[4] ≥ 0)

  
  
  We simplified constraint (70) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (71)    (x3[4] ≥ 0∧x0[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)Bound*bni_38] + [bni_38]x3[4] + [bni_38]x0[4] ≥ 0∧[1 + (-1)bso_39] + x3[4] ≥ 0)

  
  
  
• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]), COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5]), 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) which results in the following constraint:
  

  (72)    (&&(>(x3[4], 0), <=(x3[4], x0[4]))=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5])∧x3[4]=x3[5]∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2])∧x3[5]=x2[2] ⇒ COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥))

  
  
  We simplified constraint (72) using rules (I), (II), (III), (IV), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:
  

  (73)    (>(x3[4], 0)=TRUE∧<=(x3[4], x0[4])=TRUE ⇒ COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], x3[4]), x3[4]), x3[4])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥))

  
  
  We simplified constraint (73) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (74)    (x3[4] + [-1] ≥ 0∧x0[4] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x0[4] ≥ 0∧[(-1)bso_39] + x3[4] ≥ 0)

  
  
  We simplified constraint (74) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (75)    (x3[4] + [-1] ≥ 0∧x0[4] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x0[4] ≥ 0∧[(-1)bso_39] + x3[4] ≥ 0)

  
  
  We simplified constraint (75) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (76)    (x3[4] + [-1] ≥ 0∧x0[4] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x0[4] ≥ 0∧[(-1)bso_39] + x3[4] ≥ 0)

  
  
  We simplified constraint (76) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (77)    (x3[4] ≥ 0∧x0[4] + [-1] + [-1]x3[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [bni_38]x0[4] ≥ 0∧[1 + (-1)bso_39] + x3[4] ≥ 0)

  
  
  We simplified constraint (77) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (78)    (x3[4] ≥ 0∧x0[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)Bound*bni_38] + [bni_38]x3[4] + [bni_38]x0[4] ≥ 0∧[1 + (-1)bso_39] + x3[4] ≥ 0)

  
  
  
• We consider the chain 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]), COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5]), 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) which results in the following constraint:
  

  (79)    (&&(>(x3[4], 0), <=(x3[4], x0[4]))=TRUE∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5])∧x3[4]=x3[5]∧944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5])=944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4]1, 0), x3[4]1)∧x3[5]=x3[4]1 ⇒ COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5])≥NonInfC∧COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5])≥944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])∧(U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥))

  
  
  We solved constraint (79) using rules (I), (II), (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO).

To summarize, we get the following constraints P_≥ for the following pairs.

• 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) → COND_944_2_MAIN_INVOKEMETHOD(<(x1, 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2)
  
  • (x1[0] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])), ≥)∧0 = 0∧[bni_28] = 0∧[(-1)Bound*bni_28] + [bni_28]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
    
  
  
• COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0, 1), +(x1, 1)), x2), x2)
  
  • (x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)Bound*bni_30] + [bni_30]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
    
  • (x1[0] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)Bound*bni_30] + [bni_30]x1[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
    
  • (0 ≥ 0∧0 ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])), ≥)∧0 = 0∧[bni_30] = 0∧[(-1)Bound*bni_30] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
    
  
  
• 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1, 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2)
  
  • (x1[2] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])), ≥)∧0 = 0∧[bni_32] = 0∧[(-2)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)
    
  
  
• COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x1), x2), x2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0, -1), +(x1, -1)), x2), x2)
  
  • (x1[2] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧0 = 0∧[bni_34] = 0∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
    
  • (x1[2] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧0 = 0∧[bni_34] = 0∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
    
  • (x1[2] ≥ 0∧x1[2] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])), ≥)∧0 = 0∧[bni_34] = 0∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]x1[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
    
  
  
• 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0, 0), x3), x3) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3, 0), <=(x3, x0)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, 0), x3), x3)
  
  • (x3[4] ≥ 0∧x0[4] ≥ 0 ⇒ (U^Increasing(COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])), ≥)∧[(-1)Bound*bni_36] + [bni_36]x3[4] + [bni_36]x0[4] ≥ 0∧[(-1)bso_37] ≥ 0)
    
  
  
• COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0, 0), x3), x3) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0, x3), x3), x3)
  
  • (x3[4] ≥ 0∧x0[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)Bound*bni_38] + [bni_38]x3[4] + [bni_38]x0[4] ≥ 0∧[1 + (-1)bso_39] + x3[4] ≥ 0)
    
  • (x3[4] ≥ 0∧x0[4] ≥ 0 ⇒ (U^Increasing(944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])), ≥)∧[(-1)Bound*bni_38] + [bni_38]x3[4] + [bni_38]x0[4] ≥ 0∧[1 + (-1)bso_39] + x3[4] ≥ 0)
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = [3]   
POL(944_2_MAIN_INVOKEMETHOD(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁   
POL(944_1_mod_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁   
POL(944_0_minus_EQ(x₁, x₂)) = [-1] + [-1]x₂ + x₁   
POL(COND_944_2_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂   
POL(<(x₁, x₂)) = [-1]   
POL(0) = 0   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(1) = [1]   
POL(COND_944_2_MAIN_INVOKEMETHOD1(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂   
POL(>(x₁, x₂)) = [-1]   
POL(-1) = [-1]   
POL(COND_944_2_MAIN_INVOKEMETHOD2(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂   
POL(&&(x₁, x₂)) = [-1]   
POL(<=(x₁, x₂)) = [-1]   

The following pairs are in P_>:

COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])

The following pairs are in P_bound:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])
COND_944_2_MAIN_INVOKEMETHOD2(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], 0), x3[5]), x3[5]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[5], x3[5]), x3[5]), x3[5])

The following pairs are in P_≥:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(<(x1[0], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])
COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[1], 1), +(x1[1], 1)), x2[1]), x2[1])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(>(x1[2], 0), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])
COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(+(x0[3], -1), +(x1[3], -1)), x2[3]), x2[3])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(&&(>(x3[4], 0), <=(x3[4], x0[4])), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])

At least the following rules have been oriented under context sensitive arithmetic replacement:

FALSE¹ → &&(TRUE, FALSE)¹
FALSE¹ → &&(FALSE, TRUE)¹

(6) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(0): 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(x1[0] < 0, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])
(1): COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]), x2[1])
(2): 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(x1[2] > 0, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])
(3): COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]), x2[3])
(4): 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4]) → COND_944_2_MAIN_INVOKEMETHOD2(x3[4] > 0 && x3[4] <= x0[4], 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]), x3[4])

(1) -> (0), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]))∧(x2[1] →^* x2[0]))

(3) -> (0), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]))∧(x2[3] →^* x2[0]))

(0) -> (1), if ((x1[0] < 0 →^* TRUE)∧(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]))∧(x2[0] →^* x2[1]))

(1) -> (2), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]))∧(x2[1] →^* x2[2]))

(3) -> (2), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]))∧(x2[3] →^* x2[2]))

(2) -> (3), if ((x1[2] > 0 →^* TRUE)∧(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]))∧(x2[2] →^* x2[3]))

(1) -> (4), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]))∧(x2[1] →^* x3[4]))

(3) -> (4), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[4], 0), x3[4]))∧(x2[3] →^* x3[4]))

The set Q is empty.

(7) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(8) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
||	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_944_2_MAIN_INVOKEMETHOD1(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]), x2[3])
(2): 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(x1[2] > 0, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])
(1): COND_944_2_MAIN_INVOKEMETHOD(TRUE, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]), x2[1])
(0): 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(x1[0] < 0, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])

(1) -> (0), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]))∧(x2[1] →^* x2[0]))

(3) -> (0), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]))∧(x2[3] →^* x2[0]))

(0) -> (1), if ((x1[0] < 0 →^* TRUE)∧(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]))∧(x2[0] →^* x2[1]))

(1) -> (2), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1] + 1, x1[1] + 1), x2[1]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]))∧(x2[1] →^* x2[2]))

(3) -> (2), if ((944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3] + -1, x1[3] + -1), x2[3]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]))∧(x2[3] →^* x2[2]))

(2) -> (3), if ((x1[2] > 0 →^* TRUE)∧(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]) →^* 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]))∧(x2[2] →^* x2[3]))

The set Q is empty.

(9) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(greater_int(x1[2], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(less_int(x1[0], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greater_int(pos(01), pos(01)) → false
greater_int(pos(01), neg(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(neg(01), neg(01)) → false
greater_int(pos(01), pos(s(y))) → false
greater_int(neg(01), pos(s(y))) → false
greater_int(pos(01), neg(s(y))) → true
greater_int(neg(01), neg(s(y))) → true
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false
greater_int(pos(s(x)), neg(01)) → true
greater_int(neg(s(x)), neg(01)) → false
greater_int(pos(s(x)), neg(s(y))) → true
greater_int(neg(s(x)), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(neg(s(x)), neg(s(y))) → greater_int(neg(x), neg(y))
less_int(pos(01), pos(01)) → false
less_int(pos(01), neg(01)) → false
less_int(neg(01), pos(01)) → false
less_int(neg(01), neg(01)) → false
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(pos(01), neg(s(y))) → false
less_int(neg(01), neg(s(y))) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(s(x)), neg(01)) → false
less_int(neg(s(x)), neg(01)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

(11) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(greater_int(x1[2], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2])
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(less_int(x1[0], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])

The TRS R consists of the following rules:

less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

(13) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) → COND_944_2_MAIN_INVOKEMETHOD1(greater_int(x1[2], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[2], x1[2]), x2[2]), x2[2]) at position [0] we obtained the following new rules [LPAR04]:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(01)), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(01)), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(01)), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(01)), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(less_int(x1[0], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(01)), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(01)), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(01)), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(01)), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)

The TRS R consists of the following rules:

less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

(15) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(less_int(x1[0], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])

The TRS R consists of the following rules:

less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greater_int(pos(01), pos(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

(17) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(less_int(x1[0], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])

The TRS R consists of the following rules:

plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

(19) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(less_int(x1[0], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0])
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])

The TRS R consists of the following rules:

plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

(21) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) → COND_944_2_MAIN_INVOKEMETHOD(less_int(x1[0], pos(01)), 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[0], x1[0]), x2[0]), x2[0]) at position [0] we obtained the following new rules [LPAR04]:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(01)), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(01)), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(01)), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(01)), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(01)), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(01)), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(01)), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(01)), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(false, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)

The TRS R consists of the following rules:

plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

(23) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])

The TRS R consists of the following rules:

plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

(25) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.

(27) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3])
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(29) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[3], x1[3]), x2[3]), x2[3]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), x0[3]), plus_int(neg(s(01)), x1[3])), x2[3]), x2[3]) at position [0,0,1] we obtained the following new rules [LPAR04]:

COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), y0), minus_nat(x1, s(01))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), y0), neg(plus_nat(s(01), x1))), y2), y2)

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), y0), minus_nat(x1, s(01))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), y0), neg(plus_nat(s(01), x1))), y2), y2)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(31) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), y0), minus_nat(x1, s(01))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1])

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(33) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(x0[1], x1[1]), x2[1]), x2[1]) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), x0[1]), plus_int(pos(s(01)), x1[1])), x2[1]), x2[1]) at position [0,0,1] we obtained the following new rules [LPAR04]:

COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), y0), minus_nat(s(01), x1)), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), y0), pos(plus_nat(s(01), x1))), y2), y2)

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), y0), minus_nat(x1, s(01))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), y0), minus_nat(s(01), x1)), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), y0), pos(plus_nat(s(01), x1))), y2), y2)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), y0), minus_nat(x1, s(01))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), y0), minus_nat(s(01), x1)), y2), y2)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(37) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), y0), minus_nat(x1, s(01))), y2), y2) we obtained the following new rules [LPAR04]:

COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(s(z1), s(01))), z2), z2)

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), y0), minus_nat(s(01), x1)), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(s(z1), s(01))), z2), z2)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(39) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(s(z1), s(01))), z2), z2) at position [0,0,1] we obtained the following new rules [LPAR04]:

COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(z1, 01)), z2), z2)

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), y0), minus_nat(s(01), x1)), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(z1, 01)), z2), z2)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(41) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(x1)), y2), y2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), y0), minus_nat(s(01), x1)), y2), y2) we obtained the following new rules [LPAR04]:

COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, neg(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), z0), minus_nat(s(01), s(z1))), z2), z2)

(42) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(z1, 01)), z2), z2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, neg(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), z0), minus_nat(s(01), s(z1))), z2), z2)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(43) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, neg(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), z0), minus_nat(s(01), s(z1))), z2), z2) at position [0,0,1] we obtained the following new rules [LPAR04]:

COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, neg(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), z0), minus_nat(01, z1)), z2), z2)

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(z1, 01)), z2), z2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, neg(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), z0), minus_nat(01, z1)), z2), z2)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(45) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

minus_nat(s(x), s(y)) → minus_nat(x, y)

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 0   
POL(944_0_minus_EQ(x₁, x₂)) = x₁ + x₂   
POL(944_1_mod_InvokeMethod(x₁, x₂)) = x₁ + x₂   
POL(944_2_MAIN_INVOKEMETHOD(x₁, x₂)) = x₁ + x₂   
POL(COND_944_2_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(COND_944_2_MAIN_INVOKEMETHOD1(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(minus_nat(x₁, x₂)) = x₁ + x₂   
POL(neg(x₁)) = x₁   
POL(plus_int(x₁, x₂)) = x₁ + x₂   
POL(plus_nat(x₁, x₂)) = x₁ + x₂   
POL(pos(x₁)) = x₁   
POL(s(x₁)) = 1 + x₁   
POL(true) = 0   

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(z1, 01)), z2), z2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, neg(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), z0), minus_nat(01, z1)), z2), z2)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(47) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

plus_nat(s(x), y) → s(plus_nat(x, y))

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 0   
POL(944_0_minus_EQ(x₁, x₂)) = x₁ + 2·x₂   
POL(944_1_mod_InvokeMethod(x₁, x₂)) = x₁ + x₂   
POL(944_2_MAIN_INVOKEMETHOD(x₁, x₂)) = x₁ + 2·x₂   
POL(COND_944_2_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = x₁ + x₂ + 2·x₃   
POL(COND_944_2_MAIN_INVOKEMETHOD1(x₁, x₂, x₃)) = 2·x₁ + x₂ + 2·x₃   
POL(minus_nat(x₁, x₂)) = x₁ + x₂   
POL(neg(x₁)) = x₁   
POL(plus_int(x₁, x₂)) = 2·x₁ + x₂   
POL(plus_nat(x₁, x₂)) = 2·x₁ + x₂   
POL(pos(x₁)) = x₁   
POL(s(x₁)) = 1 + x₁   
POL(true) = 0   

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(z1, 01)), z2), z2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, neg(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), z0), minus_nat(01, z1)), z2), z2)

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(49) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, pos(s(x0))), y2), y2)
944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2) → COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(y0, neg(s(x0))), y2), y2)
COND_944_2_MAIN_INVOKEMETHOD1(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, pos(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(neg(s(01)), z0), minus_nat(z1, 01)), z2), z2)
COND_944_2_MAIN_INVOKEMETHOD(true, 944_1_mod_InvokeMethod(944_0_minus_EQ(z0, neg(s(z1))), z2), z2) → 944_2_MAIN_INVOKEMETHOD(944_1_mod_InvokeMethod(944_0_minus_EQ(plus_int(pos(s(01)), z0), minus_nat(01, z1)), z2), z2)

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 0   
POL(944_0_minus_EQ(x₁, x₂)) = x₁ + 2·x₂   
POL(944_1_mod_InvokeMethod(x₁, x₂)) = 1 + 2·x₁ + x₂   
POL(944_2_MAIN_INVOKEMETHOD(x₁, x₂)) = 2 + 2·x₁ + x₂   
POL(COND_944_2_MAIN_INVOKEMETHOD(x₁, x₂, x₃)) = 1 + 2·x₁ + 2·x₂ + x₃   
POL(COND_944_2_MAIN_INVOKEMETHOD1(x₁, x₂, x₃)) = 1 + 2·x₁ + 2·x₂ + x₃   
POL(minus_nat(x₁, x₂)) = x₁ + x₂   
POL(neg(x₁)) = x₁   
POL(plus_int(x₁, x₂)) = x₁ + x₂   
POL(plus_nat(x₁, x₂)) = x₁ + x₂   
POL(pos(x₁)) = x₁   
POL(s(x₁)) = 2 + 2·x₁   
POL(true) = 0   

(50) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))

The set Q consists of the following terms:

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(51) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(52) YES